\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, $e$:E, $P$, $R$:(\{$e$:E$\mid$ loc($e$) $=$ $i$ \}$\rightarrow$Prop).
\\[0ex]($\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ Dec($R$($e$)))
\\[0ex]$\Rightarrow$ (\=es{-}first{-}at{-}since(${\it es}$;$i$;$e$;$e$.$R$($e$);$e$.$P$($e$))\+
\\[0ex]$\Leftrightarrow$
\\[0ex]loc($e$) $=$ $i$
\\[0ex]\& \=$P$($e$) \& $\neg$$R$($e$)\+
\\[0ex]\& (\=($\exists$${\it e''}$:E. (${\it e''}$ $<$loc $e$) \& $P$(${\it e''}$))\+
\\[0ex]$\Rightarrow$ (\=$\exists$${\it e'}$:E.\+
\\[0ex](${\it e'}$ $<$loc $e$)
\\[0ex]\& $R$(${\it e'}$) \& ($\forall$${\it e''}$:E. (${\it e'}$ $<$loc ${\it e''}$) $\Rightarrow$ (${\it e''}$ $<$loc $e$) $\Rightarrow$ $\neg$$P$(${\it e''}$) \& $\neg$$R$(${\it e''}$)))))
\-\-\-\-
\end{tabbing}